(** LÃ³gica Computacional 1 *)

Section Listas.

(** 1. Defina indutivamente o tipo 'listnat' para representar listas de
   naturais. *)
  
  Inductive listnat : Set := 
  | nil : listnat
  | cons : nat -> listnat -> listnat. 


(** 2. Defina o predicado 'ordenada: listnat -> Prop' que caracteriza
   listas de nÃºmeros naturais ordenadas de forma crescente. *)

  Inductive ordenada :listnat -> Prop :=
  | lista_vazia : ordenada nil
  | lista_1: forall n:nat, ordenada (cons n nil)
  | lista_nv : forall (x y: nat) (l:listnat), ordenada (cons y l) -> x <= y -> ordenada (cons x (cons y l)).


Lemma l_trivial : ordenada nil.
Proof.
apply lista_vazia.
Qed.


Lemma lu_ordenada : ordenada (cons 7 nil).
Proof.
(*COMPLETAR*)
apply lista_1.
Qed.

Lemma lnv_ordenada : ordenada (cons 1 (cons 2 (cons 3 (cons 3 nil)))).
Proof.
(*COMPLETAR*)
apply lista_nv.
apply lista_nv.
apply lista_nv.
apply lista_1.
auto.
auto.
auto.
Qed.




(** 3. Duas listas sÃ£o equivalentes se possuem os mesmos
   elementos. Esta noÃ§Ã£o serÃ¡ especificada baseada no nÃºmero de
   ocorrÃªncias de um elemento na lista. Construa a funÃ§Ã£o 'num_oc: nat
   -> listnat -> nat' que recebe como argumento um natural n, uma
   lista l e retorna o nÃºmero de ocorrÃªncias de n em l.*)

Require Import Compare_dec.

Fixpoint num_oc n l {struct l} := match l with
                                   | nil => 0
                                   | cons h tl => match nat_compare n h with
                                                    | Eq => S(num_oc n tl) 
                                                    | _ => num_oc n tl 
                                                  end
                                  end.

Eval compute in (num_oc 2 (cons 2 (cons 2 (cons 2 (cons 1 nil))))).

  (** Baseado no exercÃ­cio anterior podemos definir a equivalÃªncia
     entre listas. *)

Definition equiv l l' := forall n:nat, num_oc n l = num_oc n l'.

(** 4. Prove que 'equiv' Ã© uma relaÃ§Ã£o de equivalÃªncia. Ou seja, prove
   os teoremas 'equiv_refl', 'equiv_sym' e 'equiv_trans' a seguir. *)

Theorem equiv_refl : forall l:listnat, equiv l l.
Proof.
 (*COMPLETAR*)
intro l.
unfold equiv.
auto.
Qed.

Theorem equiv_sym : forall (l l':listnat), equiv l l' -> equiv l' l.
Proof.
  (*COMPLETAR*)
induction l.
intros l'.
unfold equiv.
trivial.
intro h.
symmetry.
trivial.
intro l'.
unfold equiv.
intros.
symmetry.
auto.
Qed.
  
Theorem equiv_trans: forall (l l' l'':listnat), equiv l l' -> equiv l' l'' -> equiv l l''.
Proof.
  (*COMPLETAR*)

Qed.





(** 5. Prove que qualquer lista de nÃºmeros naturais pode ser ordenada. Isto Ã©, prove o seguinte teorema: *)

 (*OBS.: Para provar este teorema, funÃ§Ãµes e lemas auxiliares podem ser definidos!*)

Theorem ordem : forall l:listnat, {l':listnat | equiv l l' /\ ordenada l'}.
Proof.
  (*COMPLETAR*)
Qed.

End Listas.

Extraction ordem.